$\forall$${\it es}$:ES, $A$:Type, ${\it Ia}$:AbsInterface($A$), $Q$:(E$\rightarrow$E$\rightarrow\mathbb{P}$). $\lambda$$e$.$e$ glues ${\it Ia}$:$Q$ $--\lambda$$e$.${\it Ia}$($e$)$\rightarrow$ ${\it Ia}$:$Q$